interface-union(X;Y)
== <fpf-domain(X) @ fpf-domain(Y)
== , ik,s,v. if ik  dom(X)
== , then if ik  dom(Y)
== , then then case X(ik)(s,v)
== , then then of inl(x) => inl inl x  
== , then then o| inr(x) => case Y(ik)(s,v) of inl(x) => inl (inr x )  | inr(x) => inr x 
== , then else case X(ik)(s,v) of inl(x) => inl inl x   | inr(x) => inr x 
== , then fi 
== , else case Y(ik)(s,v) of inl(x) => inl (inr x )  | inr(x) => inr x 
== , fi 
== > 

latex

---

clarification:

interface-union(X;Y)
== <fpf-domain(X) @ fpf-domain(Y)
== , ik,s,v. if fpf-dom(locknd-deq(); ik; X)
== , then if fpf-dom(locknd-deq(); ik; Y)
== , then then case Xlocknd-deq()(ik)(s,v)
== , then then of inl(x) => inl inl x  
== , then then o| inr(x) => case Ylocknd-deq()(ik)(s,v)
== , then then o| inr(x) => of inl(x) => inl (inr x ) 
== , then then o| inr(x) => o| inr(x) => inr x 
== , then else case Xlocknd-deq()(ik)(s,v) of inl(x) => inl inl x   | inr(x) => inr x 
== , then fi 
== , else case Ylocknd-deq()(ik)(s,v) of inl(x) => inl (inr x )  | inr(x) => inr x 
== , fi 
== > 

latex

Definitions	<a, b>, as @ bs, fpf-domain(f), x.A(x), if b then t else f fi , x  dom(f), case b of inl(x) => s(x) | inr(y) => t(y), f(a), f(x), locknd-deq(), inl x , inr x
FDL editor aliases	interface-union